\subsection{Exceptions and Software-generated Interrupts}
As outlined in section \ref{subsec:design-exceptions}, exceptions in the kernel
running in VMX root mode should not happen because it is implemented in SPARK
and absence of runtime errors has been proven.  This section describes the
handling of exceptions or software-generated interrupts\footnote{As raised by
the \texttt{int} instruction.} caused by subject code. The behavior on
exceptions in VMX non-root mode is determined by the subject profile (VM or
Native).

For subjects running in the VM profile, the exception bitmap inside the VMCS
structure is set to zero. This has the effect that exceptions and
Software-generated interrupts do not result in a trap. VM subjects must
implement their own exception handling, only a triple fault inside a subject
leads to a trap into the kernel.

For native subjects, the VMCS exception bitmap field is set to the value
\texttt{0xffffffff} which causes a trap if any exception or Software-generated
interrupt is caused by the subject. As described in section \ref{subsec:traps},
a trap is forwarded to a handler subject by configuring the subject's trap
table appropriately. A subject monitor can react to the exception and resume
the causing subject after the error condition has been removed.

To make sure non-maskable interrupts\footnote{NMIs are (mostly) used to signal
attention for non-recoverable hardware errors.} (NMI\index{NMI}) are not
handled by subjects but lead to a VM exit unconditionally, the "NMI exiting"
VMX execution control is active in both subject profiles. On reception of an
NMI, the kernel halts the CPU.
